@jdchristensen I thought I redefined the proofs in pHomotopy to be wildcat proofs which should unfold to the ones in core.

1. Regardless of how things unfold, we shouldn't have redundant lemmas, so we'll need to decide which version to keep and where to keep it.

2. The proofs in pHomotopy.v, using WildCat, certainly won't unfold to be the same as the proofs in Core.v. The proofs in Core.v use path induction, for example. But I don't think this is a relevant point. We should just keep whichever is best.

3. Before this commit, the universe variables were quite different. In Core.v, the three pointed types could have independent universes, while in pHomotopy.v, they had to be the same. In theory, this shouldn't matter, but in practice, forcing them to be the same causes problems with Coq choosing the universe variables. This commit fixes that issue.

However, after this commit, the proof in pHomotopy.v needs five universe variables, one for each type, one as an upper bound, and one strictly greater, for the WildCat instances. The proof in Core needs exactly three. Because of this, I think we should stick with the proof in Core, and remove the WildCat proof. As usual, the reason is that those two extra variables are free, and might accumulate. Sound good?

(I really wish we could use u+1 and max(u,v) in various places to avoid free universe variables that accumulate... It would simplify many workarounds we have, and would also allow us to use WildCats more freely.)

I went ahead and removed the versions in pHomotopy.v. I've also pushed other changes related to the interplay between WildCat and pointed types. The changes to ExactSequence avoid the extra "WildCat" universe variable for some results (where it was just a matter of changing notation), and in those cases the universe variables for the input types become free, whereas before several of them (but not all) were constrained to be equal, which made it hard for Coq to guess the correct universe variables.

I've now marked this PR as ready for review.

Incidentally, pHomotopy.v is very short, and could just be merged into Core.v.

I think it makes sense for phomotopy to be merged. If I recall correctly it was split out before we had wild cats, so it made sense to grpup such lemmas in once place. Now we don't really need any of them.

Everything here looks good.

Regarding the changing of notation from $ to * in ExactSequence, I've wondered for some time if it might make sense to generalize everything there from pType to a generic pointed category. This should encompass exactness for Grp, Ab, any abelian category, pointed types, spectra etc. The only missing component seems to a notion of wild cat with small limits like fibers/kernels. This would also allow us to easily talk about left-exact functors which might be useful for describing properties of the homotopy group functors.

I think it makes sense for phomotopy to be merged.

I agree, and I've now merged pHomotopy.v into Core.v. The first of the new commits simplifies pHomotopy.v in place (including removing Univalence from one result). The second makes some minor changes to Pointed/Core.v, removing one redundant result and updating lots of comments. The third commit does the merge, but it requires reordering a lot of things in Pointed/Core.v. There are no non-trivial changes, but the diff is large, so you'll need to review the commits separately. The fourth commit just removes three Local Existing Instance declarations that are redundant.

I'll wait for another review of these four commits.

I think there's still a lot of room for simplifying Pointed/Core.v, but it will need to be balanced against the challenges involving universe variables that arise when using WildCat.

I also agree that ExactSequence could probably be done in any WildCat, but I'm not going to tackle that.